consensus.4.jani:model: info: consensus.4 is an MDP model and will be simulated as an MDP.
consensus.4.jani:variables[6]: info: Expanding variable "pc1" into 4 locations in automaton "process1".
consensus.4.jani:variables[8]: info: Expanding variable "pc2" into 4 locations in automaton "process2".
consensus.4.jani:variables[10]: info: Expanding variable "pc3" into 4 locations in automaton "process3".
consensus.4.jani:variables[12]: info: Expanding variable "pc4" into 4 locations in automaton "process4".
consensus.4.jani: info: Using default value of 0.95 for the confidence parameter.
consensus.4.jani: warning: Using the Chow-Robbins method for relative-width sequential confidence intervals, which guarantees the requested confidence only asymptotically for decreasing width.
Peak memory usage: 59 MB
Analysis results for consensus.4.jani
Experiment K=4
Status: Finished
Simulation time: 599.5 s
+ Property Property "steps_min"
Estimated min. value: 849.1801788375557
Min. confidence interval: [832.2121424755067, 866.1482151996047]
Runs used (best scheduler): 6710
Total runs used: 1208710
Schedulers sampled: 1000
Best scheduler: 1359056563
Run type: MDP
Status: Finished
+ Min. sample data
Mean: 849.1801788375557
Variance: 502909.11896911374
Skewness: 2.0081866846939294
Kurtosis: 9.099955213849022
+ Error bounds
Scheduler sampling: The result is an upper bound for the true min. value.
Statement: CI: 100(1 - α)% of intervals contain true value (CLT assumption)
α: 0.050000000000000044